\chapter{Inleiding}
\label{chap:inl}

\npar Naar aanleiding van de komst van een zware crimineel wil de
directie van de gevangenis zeker zijn dat alle veligheidsprotocollen volledig
werken. Daarom werd er een onafhankelijke verificatie doorgevoerd van de
verschillende protocollen. 

\npar Deze verificatie werd in 2 talen gemodelleerd. In het eerste hoofdstuk
wordt het ontwerp in IDP besproken. Hierbij worden verschillende
ontwerpbeslissingen toegelicht

\npar In het 2e hoofdstuk wordt de modellering in NuSMV op een analoge
manier uitgelegd.

\npar In een laatste hoofdstuk worden de ervaringen met beide talen besproken.
Hier worden ook nog algemene problemen aangehaald bij het modelleren van de
verschillende talen. 
